
# To normalize:
# bibtool --preserve.key.case=on --preserve.keys=on --pass.comments=on --print.use.tab=off -s -i docs/references.bib -o docs/references.bib

# https://www.zbmath.org/ and https://mathscinet.ams.org/mathscinet
# (or the free tool https://mathscinet.ams.org/mrlookup)
# are good sources of complete bibtex entries for mathematics

# To link to an entry in `references.bib`, use the following formats:
#   [Author, *Title* (optional location)][bibkey]
@InProceedings{   adhesive2004,
  author        = {S. Lack and P. Soboci{\'n}ski},
  title         = {Adhesive categories},
  booktitle     = {Foundations of Software Science and Computation
                  Structures, {FoSSaCS '04}},
  series        = {LNCS},
  volume        = {2987},
  pages         = {273--288},
  publisher     = {Springer},
  year          = {2004},
  url           = {https://www.ioc.ee/~pawel/papers/adhesive.pdf}
}

@Article{         ahrens2017,
  author        = {Benedikt Ahrens and Peter LeFanu Lumsdaine},
  year          = {2019},
  title         = {Displayed Categories},
  journal       = {Logical Methods in Computer Science},
  volume        = {15},
  issue         = {1},
  doi           = {10.23638/LMCS-15(1:20)2019}
}

@Article{         aigner1999proofs,
  author        = {Aigner, Martin and Ziegler, G{\"u}nter M},
  title         = {Proofs from THE BOOK},
  journal       = {Berlin. Germany},
  year          = {1999},
  publisher     = {Springer}
}

@Article{         alfseneffros1972,
  author        = {Erik M. {Alfsen} and Edward G. {Effros}},
  title         = {{Structure in real Banach spaces. I and II}},
  fjournal      = {{Annals of Mathematics. Second Series}},
  journal       = {{Ann. Math. (2)}},
  issn          = {0003-486X},
  volume        = {96},
  pages         = {98--173},
  year          = {1972},
  publisher     = {Princeton University, Mathematics Department, Princeton,
                  NJ},
  language      = {English},
  doi           = {10.2307/1970895},
  msc2010       = {46L05 46B10 46K05 46E15 46B99 46A40},
  zbl           = {0248.46019}
}

@Book{            alfsenshultz2003,
  author        = {Erik M. {Alfsen} and Frederic W. {Shultz}},
  title         = {{Geometry of state spaces of operator algebras}},
  isbn          = {0-8176-4319-2},
  pages         = {xiii + 467},
  year          = {2003},
  publisher     = {Boston, MA: Birkh\"auser},
  language      = {English},
  msc2010       = {46-02 46L05 46L10 46L70 46L30 17C65},
  zbl           = {1042.46001}
}

@Book{            aluffi2016,
  title         = {Algebra: Chapter 0},
  author        = {Aluffi, Paolo},
  series        = {Graduate Studies in Mathematics},
  volume        = {104},
  year          = {2016},
  publisher     = {American Mathematical Society},
  edition       = {Reprinted with corrections by the American Mathematical
                  Society}
}

@Book{            atiyah-macdonald,
  author        = {Atiyah, M. F. and Macdonald, I. G.},
  title         = {Introduction to commutative algebra},
  publisher     = {Addison-Wesley Publishing Co., Reading, Mass.-London-Don
                  Mills, Ont.},
  year          = {1969},
  pages         = {ix+128},
  mrclass       = {13.00},
  mrnumber      = {0242802},
  mrreviewer    = {J. A. Johnson}
}

@InProceedings{   avigad-carneiro-hudon2019,
  author        = {Jeremy Avigad and Mario M. Carneiro and Simon Hudon},
  editor        = {John Harrison and John O'Leary and Andrew Tolmach},
  title         = {Data Types as Quotients of Polynomial Functors},
  booktitle     = {10th International Conference on Interactive Theorem
                  Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
                  {USA}},
  series        = {LIPIcs},
  volume        = {141},
  pages         = {6:1--6:19},
  publisher     = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year          = {2019},
  url           = {https://doi.org/10.4230/LIPIcs.ITP.2019.6},
  doi           = {10.4230/LIPIcs.ITP.2019.6},
  timestamp     = {Fri, 27 Sep 2019 15:57:06 +0200},
  biburl        = {https://dblp.org/rec/conf/itp/AvigadCH19.bib},
  bibsource     = {dblp computer science bibliography, https://dblp.org}
}

@Misc{            avigad_moura_kong-2017,
  author        = {Jeremy Avigad and Leonardo de Moura and Soonho Kong},
  title         = {{T}heorem {P}roving in {L}ean},
  year          = {2017},
  howpublished  = {\url{https://leanprover.github.io/theorem_proving_in_lean/}}
}

@Book{            axler2015,
  author        = {Sheldon Axler},
  title         = {Linear algebra done right. 3rd ed.},
  fjournal      = {Undergraduate Texts in Mathematics},
  journal       = {Undergraduate Texts Math.},
  issn          = {0172-6056; 2197-5604/e},
  edition       = {3rd ed.},
  isbn          = {978-3-319-11079-0/hbk; 978-3-319-11080-6/ebook},
  pages         = {xvii + 340},
  year          = {2015},
  publisher     = {Springer}
}

@Manual{          banasiak,
  author        = {Banasiak},
  title         = {Banach Lattices in Applications},
  organization  = {University of Pretoria},
  address       = {Pretoria, South Africa}
}

@Book{            beals2004,
  author        = {Richard Beals},
  title         = {Analysis. An introduction},
  publisher     = {Cambridge University Press},
  isbn          = {0521600472},
  year          = {2004}
}

@Book{            behrends1979,
  author        = {Ehrhard {Behrends}},
  title         = {{M-structure and the Banach-Stone theorem}},
  fjournal      = {{Lecture Notes in Mathematics}},
  journal       = {{Lect. Notes Math.}},
  issn          = {0075-8434},
  volume        = {736},
  year          = {1979},
  publisher     = {Springer, Cham},
  language      = {English},
  msc2010       = {46B20 46-02 46E40 46A40},
  zbl           = {0436.46013}
}

@Book{            berger1987,
  author        = {Marcel Berger},
  title         = {Geometry I},
  publisher     = {Springer Berlin},
  year          = 1987,
  issn          = {0172-5939},
  pages         = {XIV, 432},
  series        = {Universitext},
  address       = {Heidelberg},
  edition       = 1
}

@Article{         bernstein1912,
  author        = {Bernstein, S.},
  year          = {1912},
  title         = {Démonstration du théorème de Weierstrass fondée sur le
                  calcul des probabilités},
  journal       = {Comm. Kharkov Math. Soc.},
  volume        = {13},
  number        = {1–2}
}

@InProceedings{   beylin1996,
  author        = "Beylin, Ilya and Dybjer, Peter",
  editor        = "Berardi, Stefano and Coppo, Mario",
  title         = "Extracting a proof of coherence for monoidal categories
                  from a proof of normalization for monoids",
  booktitle     = "Types for Proofs and Programs",
  year          = "1996",
  publisher     = "Springer Berlin Heidelberg",
  address       = "Berlin, Heidelberg",
  pages         = "47--61",
  abstract      = "This paper studies the problem of coherence in category
                  theory from a type-theoretic viewpoint. We first show how a
                  Curry-Howard interpretation of a formal proof of
                  normalization for monoids almost directly yields a
                  coherence proof for monoidal categories. Then we formalize
                  this coherence proof in intensional intuitionistic type
                  theory and show how it relies on explicit reasoning about
                  proof objects for intensional equality. This formalization
                  has been checked in the proof assistant ALF.",
  isbn          = "978-3-540-70722-6"
}

@Book{            billingsley1999,
  author        = {Billingsley, Patrick},
  title         = {Convergence of probability measures},
  series        = {Wiley Series in Probability and Statistics: Probability
                  and Statistics},
  edition       = {Second},
  note          = {A Wiley-Interscience Publication},
  publisher     = {John Wiley \& Sons, Inc., New York},
  year          = {1999},
  pages         = {x+277},
  isbn          = {0-471-19745-9},
  mrclass       = {60B10 (28A33 60F17)},
  mrnumber      = {1700749},
  doi           = {10.1002/9780470316962},
  url           = {https://doi.org/10.1002/9780470316962}
}

@Article{         birkhoff1942,
  author        = {Birkhoff, Garrett},
  title         = {Lattice, ordered groups},
  journal       = {Ann. of Math. (2)},
  fjournal      = {Annals of Mathematics. Second Series},
  volume        = {43},
  year          = {1942},
  pages         = {298--331},
  issn          = {0003-486X},
  mrclass       = {20.0X},
  mrnumber      = {6550},
  mrreviewer    = {H. Wallman},
  doi           = {10.2307/1968871},
  url           = {https://doi.org/10.2307/1968871}
}

@Book{            bollobas1986,
  author        = {Bollob\'{a}s, B\'{e}la},
  title         = {Combinatorics: Set Systems, Hypergraphs, Families of
                  Vectors, and Combinatorial Probability},
  year          = {1986},
  isbn          = {0521330599},
  publisher     = {Cambridge University Press}
}

@Book{            borceux-vol1,
  title         = {Handbook of Categorical Algebra: Volume 1, Basic Category
                  Theory},
  author        = {Borceux, Francis},
  series        = {Encyclopedia of Mathematics},
  volume        = {50},
  year          = {1994},
  publisher     = {Cambridge University Press}
}

@Book{            borceux-vol2,
  title         = {Handbook of Categorical Algebra: Volume 2, Categories and
                  Structures},
  author        = {Borceux, Francis},
  series        = {Encyclopedia of Mathematics},
  volume        = {51},
  year          = {1994},
  publisher     = {Cambridge University Press}
}

@Book{            borceux-vol3,
  title         = {Handbook of Categorical Algebra: Volume 3, Sheaf Theory},
  author        = {Borceux, Francis},
  series        = {Encyclopedia of Mathematics},
  volume        = {52},
  year          = {1994},
  publisher     = {Cambridge University Press}
}

@Book{            bosch-guntzer-remmert,
  title         = {Non-Archimedean Analysis : A Systematic Approach to Rigid
                  Analytic Geometry},
  author        = {S. Bosch and U. G{\"{u}}ntzer and R. Remmert},
  series        = {Grundlehren der mathematischen Wissenschaften},
  volume        = {261},
  year          = {1984},
  publisher     = {Springer-Verlag Berlin }
}

@Book{            bourbaki1966,
  author        = {Bourbaki, Nicolas},
  title         = {Elements of mathematics. {G}eneral topology. {P}art 1},
  publisher     = {Hermann, Paris; Addison-Wesley Publishing Co., Reading,
                  Mass.-London-Don Mills, Ont.},
  year          = {1966},
  pages         = {vii+437},
  mrclass       = {54.00 (00.00)},
  mrnumber      = {0205210}
}

@Book{            bourbaki1966b,
  author        = {Bourbaki, Nicolas},
  title         = {Elements of mathematics. {G}eneral topology. {P}art 2},
  publisher     = {Hermann, Paris; Addison-Wesley Publishing Co., Reading,
                  Mass.-London-Don Mills, Ont.},
  year          = {1966},
  pages         = {iv+363},
  mrclass       = {54-02 (00A05 54-01)},
  mrnumber      = {979295}
}

@Book{            bourbaki1968,
  author        = {Bourbaki, Nicolas},
  title         = {Lie groups and {L}ie algebras. {C}hapters 4--6},
  series        = {Elements of Mathematics (Berlin)},
  note          = {Translated from the 1968 French original by Andrew
                  Pressley},
  publisher     = {Springer-Verlag, Berlin},
  year          = {2002},
  pages         = {xii+300},
  isbn          = {3-540-42650-7},
  mrclass       = {17-01 (00A05 20E42 20F55 22-01)},
  mrnumber      = {1890629}
}

@Book{            bourbaki1975,
  author        = {Bourbaki, Nicolas},
  title         = {Lie groups and {L}ie algebras. {C}hapters 1--3},
  series        = {Elements of Mathematics (Berlin)},
  note          = {Translated from the French, Reprint of the 1989 English
                  translation},
  publisher     = {Springer-Verlag, Berlin},
  year          = {1998},
  pages         = {xviii+450},
  isbn          = {3-540-64242-0},
  mrclass       = {17Bxx (00A05 22Exx)},
  mrnumber      = {1728312}
}

@Book{            bourbaki1975b,
  author        = {Bourbaki, Nicolas},
  title         = {Lie groups and {L}ie algebras. {C}hapters 7--9},
  series        = {Elements of Mathematics (Berlin)},
  note          = {Translated from the 1975 and 1982 French originals by
                  Andrew Pressley},
  publisher     = {Springer-Verlag, Berlin},
  year          = {2005},
  pages         = {xii+434},
  isbn          = {3-540-43405-4},
  mrclass       = {17-01 (01A75 22-01)},
  mrnumber      = {2109105}
}

@Book{            bourbaki1981,
  author        = {Bourbaki, N.},
  title         = {Algebra. {II}. {C}hapters 4--7},
  series        = {Elements of Mathematics (Berlin)},
  note          = {Translated from the French by P. M. Cohn and J. Howie},
  publisher     = {Springer-Verlag, Berlin},
  year          = {1990},
  pages         = {vii+461},
  isbn          = {3-540-19375-8},
  mrclass       = {00A05 (12-01 13-01)},
  mrnumber      = {1080964}
}

@Book{            bourbaki1987,
  author        = {Bourbaki, N.},
  title         = {Topological vector spaces. {C}hapters 1--5},
  series        = {Elements of Mathematics (Berlin)},
  note          = {Translated from the French by H. G. Eggleston and S.
                  Madan},
  publisher     = {Springer-Verlag, Berlin},
  year          = {1987},
  pages         = {viii+364},
  isbn          = {3-540-13627-4},
  mrclass       = {46-02 (46-01 46Axx 47D15)},
  mrnumber      = {910295},
  doi           = {10.1007/978-3-642-61715-7},
  url           = {https://doi.org/10.1007/978-3-642-61715-7}
}

@Book{            bourbaki2007,
  author        = {Bourbaki, Nicolas},
  edition       = {Réimpression inchangée de l'édition originale de 1959},
  series        = {Eléments de mathématique},
  title         = {Algèbre. {C}hapitre IX},
  isbn          = {978-3-540-35338-6},
  language      = {fr},
  number        = {2},
  publisher     = {Springer},
  year          = {2007}
}

@Book{            boydVandenberghe2004,
  author        = {Stephen P. Boyd and Lieven Vandenberghe},
  title         = {Convex Optimization},
  publisher     = {Cambridge University Press},
  year          = {2004},
  isbn          = {978-0-521-83378-3},
  url           = {https://web.stanford.edu/~boyd/cvxbook/bv_cvxbook.pdf}
}

@Book{            brodmannsharp13,
  author        = {Brodmann, M. P. and Sharp, R. Y.},
  title         = {Local cohomology},
  series        = {Cambridge Studies in Advanced Mathematics},
  volume        = {136},
  edition       = {Second},
  note          = {An algebraic introduction with geometric applications},
  publisher     = {Cambridge University Press, Cambridge},
  year          = {2013},
  pages         = {xxii+491},
  isbn          = {978-0-521-51363-0},
  mrclass       = {13D45 (13-01)}
}

@Book{            cabreragarciarodriguezpalacios2014,
  author        = {Miguel {Cabrera Garc\'{\i}a} and \'Angel {Rodr\'{\i}guez
                  Palacios}},
  title         = {{Non-associative normed algebras. Volume 1. The
                  Vidav-Palmer and Gelfand-Naimark theorems}},
  fjournal      = {{Encyclopedia of Mathematics and Its Applications}},
  journal       = {{Encycl. Math. Appl.}},
  issn          = {0953-4806},
  volume        = {154},
  isbn          = {978-1-107-04306-0; 978-1-107-33776-3},
  pages         = {xxii + 712},
  year          = {2014},
  publisher     = {Cambridge: Cambridge University Press},
  language      = {English},
  doi           = {10.1017/CBO9781107337763},
  msc2010       = {46-02 17-02 46H70 46K70 46L70 17A15 17A80 17C65},
  zbl           = {1322.46003}
}

@Article{         cadiou1972,
  title         = {Recursive definitions of partial functions and their
                  computations},
  doi           = {10.1145/942580.807072},
  number        = {14},
  journal       = {ACM SIGACT News},
  author        = {Cadiou, Jean Marie Cadiou and Manna, Zohar},
  year          = {1972},
  month         = {Jan},
  pages         = {58–65}
}

@Book{            calugareanu,
  author        = {C\v{a}lug\v{a}reanu, Grigore},
  year          = {2000},
  month         = {01},
  pages         = {},
  title         = {Lattice Concepts of Module Theory},
  doi           = {10.1007/978-94-015-9588-9}
}

@Article{         CARBONI1993145,
  author        = {Aurelio Carboni and Stephen Lack and R.F.C. Walters},
  doi           = {https://doi.org/10.1016/0022-4049(93)90035-R},
  issn          = {0022-4049},
  journal       = {Journal of Pure and Applied Algebra},
  number        = {2},
  pages         = {145-158},
  title         = {Introduction to extensive and distributive categories},
  url           = {https://www.sciencedirect.com/science/article/pii/002240499390035R},
  volume        = {84},
  year          = {1993},
  bdsk-url-1    = {https://www.sciencedirect.com/science/article/pii/002240499390035R},
  bdsk-url-2    = {https://doi.org/10.1016/0022-4049(93)90035-R}
}

@Article{         carneiro2015arithmetic,
  title         = {Arithmetic in Metamath, Case Study: Bertrand's Postulate},
  author        = {Carneiro, Mario},
  journal       = {arXiv preprint arXiv:1503.02349},
  year          = {2015}
}

@Misc{            carneiro2018matiyasevic,
  title         = {A {L}ean formalization of {M}atiyasevi{\v c}'s theorem},
  author        = {Mario Carneiro},
  year          = {2018},
  eprint        = {1802.01795},
  archiveprefix = {arXiv},
  primaryclass  = {math.LO}
}

@InProceedings{   carneiro2019,
  author        = {Mario M. Carneiro},
  editor        = {John Harrison and John O'Leary and Andrew Tolmach},
  title         = {Formalizing Computability Theory via Partial Recursive
                  Functions},
  booktitle     = {10th International Conference on Interactive Theorem
                  Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
                  {USA}},
  series        = {LIPIcs},
  volume        = {141},
  pages         = {12:1--12:17},
  publisher     = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year          = {2019},
  url           = {https://doi.org/10.4230/LIPIcs.ITP.2019.12},
  doi           = {10.4230/LIPIcs.ITP.2019.12},
  timestamp     = {Fri, 27 Sep 2019 15:57:06 +0200},
  biburl        = {https://dblp.org/rec/conf/itp/Carneiro19.bib},
  bibsource     = {dblp computer science bibliography, https://dblp.org}
}

@Article{         cassels1950,
  author        = {Cassels, J. W. S.},
  title         = {Some metrical theorems in {D}iophantine approximation.
                  {I}},
  journal       = {Proc. Cambridge Philos. Soc.},
  fjournal      = {Proceedings of the Cambridge Philosophical Society},
  volume        = {46},
  year          = {1950},
  pages         = {209--218},
  issn          = {0008-1981},
  mrclass       = {10.0X},
  mrnumber      = {36787},
  mrreviewer    = {P. Erd\H{o}s},
  doi           = {10.1017/s0305004100025676},
  url           = {https://doi.org/10.1017/s0305004100025676}
}

@Book{            cassels1967algebraic,
  title         = {Algebraic number theory},
  author        = {Cassels, John William Scott and Fr{\"o}hlich, Albrecht},
  booktitle     = {Proceedings of an instructional conference organized by
                  the {L}ondon {M}athematical {S}ociety (a {NATO} {A}dvanced
                  {S}tudy {I}nstitute) with the support of the
                  {I}nternational {M}athematical {U}nion},
  editor        = {Cassels, John William Scott and Fr\"{o}hlich, Albrecht},
  publisher     = {Academic Press, London; Thompson Book Co., Inc.,
                  Washington, D.C.},
  year          = {1967},
  pages         = {xviii+366},
  mrclass       = {00.04 (10.00)}
}

@InProceedings{   Chou1994,
  author        = {Chou, Ching-Tsun},
  booktitle     = {Higher Order Logic Theorem Proving and Its Applications},
  title         = {A formal theory of undirected graphs in higher-order
                  logic},
  year          = {1994},
  address       = {Berlin, Heidelberg},
  editor        = {Melham, Thomas F. and Camilleri, Juanito},
  pages         = {144--157},
  publisher     = {Springer Berlin Heidelberg},
  isbn          = {978-3-540-48803-3}
}

@Book{            chu2012,
  author        = {Cho-Ho {Chu}},
  title         = {{Jordan structures in geometry and analysis}},
  fjournal      = {{Cambridge Tracts in Mathematics}},
  journal       = {{Camb. Tracts Math.}},
  issn          = {0950-6284},
  volume        = {190},
  isbn          = {978-1-107-01617-0},
  pages         = {x + 261},
  year          = {2012},
  publisher     = {Cambridge: Cambridge University Press},
  language      = {English},
  msc2010       = {17-02 17C65 17C37 46H70 53C35 46K70 32M15},
  zbl           = {1238.17001}
}

@InProceedings{   CL21,
  author        = {Commelin, Johan and Lewis, Robert Y.},
  title         = {Formalizing the Ring of Witt Vectors},
  year          = {2021},
  isbn          = {9781450382991},
  publisher     = {Association for Computing Machinery},
  address       = {New York, NY, USA},
  url           = {https://doi.org/10.1145/3437992.3439919},
  doi           = {10.1145/3437992.3439919},
  abstract      = {The ring of Witt vectors W R over a base ring R is an
                  important tool in algebraic number theory and lies at the
                  foundations of modern p-adic Hodge theory. W R has the
                  interesting property that it constructs a ring of
                  characteristic 0 out of a ring of characteristic p &gt; 1,
                  and it can be used more specifically to construct from a
                  finite field containing ℤ/pℤ the corresponding
                  unramified field extension of the p-adic numbers ℚp
                  (which is unique up to isomorphism). We formalize the
                  notion of a Witt vector in the Lean proof assistant, along
                  with the corresponding ring operations and other algebraic
                  structure. We prove in Lean that, for prime p, the ring of
                  Witt vectors over ℤ/pℤ is isomorphic to the ring of
                  p-adic integers ℤp. In the process we develop idioms to
                  cleanly handle calculations of identities between
                  operations on the ring of Witt vectors. These calculations
                  are intractable with a naive approach, and require a proof
                  technique that is usually skimmed over in the informal
                  literature. Our proofs resemble the informal arguments
                  while being fully rigorous.},
  booktitle     = {Proceedings of the 10th ACM SIGPLAN International
                  Conference on Certified Programs and Proofs},
  pages         = {264–277},
  numpages      = {14},
  keywords      = {ring theory, formal math, proof assistant, Lean, number
                  theory},
  location      = {Virtual, Denmark},
  series        = {CPP 2021}
}

@Book{            clark_gon,
  author        = {Pete L. Clark},
  title         = {Geometry of Numbers with Applications to Number Theory},
  url           = {http://alpha.math.uga.edu/~pete/geometryofnumbers.pdf}
}

@Book{            conway2001,
  author        = {Conway, J. H.},
  title         = {On numbers and games},
  edition       = {Second},
  publisher     = {A K Peters, Ltd., Natick, MA},
  year          = {2001},
  pages         = {xii+242},
  isbn          = {1-56881-127-6},
  mrclass       = {00A08 (05-01 91A05)},
  mrnumber      = {1803095}
}

@Book{            coxlittleoshea1997,
  author        = {David A. Cox and John Little and Donal O'Shea},
  title         = {Ideals, varieties, and algorithms - an introduction to
                  computational algebraic geometry and commutative algebra
                  {(2.} ed.)},
  series        = {Undergraduate texts in mathematics},
  publisher     = {Springer},
  year          = {1997},
  isbn          = {978-0-387-94680-1}
}

@Article{         crans2017,
  author        = {Crans, Alissa S. and Mukherjee, Sujoy and Przytycki,
                  J\'{o}zef H.},
  title         = {On homology of associative shelves},
  journal       = {J. Homotopy Relat. Struct.},
  fjournal      = {Journal of Homotopy and Related Structures},
  volume        = {12},
  year          = {2017},
  number        = {3},
  pages         = {741--763},
  issn          = {2193-8407},
  mrclass       = {18G60 (20M32 20N02 57M25)},
  mrnumber      = {3691304},
  mrreviewer    = {Mahender Singh},
  doi           = {10.1007/s40062-016-0164-9},
  url           = {https://doi.org/10.1007/s40062-016-0164-9}
}

@Book{            davey_priestley,
  author        = {Davey, B. A. and Priestley, H. A.},
  title         = {Introduction to lattices and order},
  edition       = {Second},
  publisher     = {Cambridge University Press, New York},
  year          = {2002},
  pages         = {xii+298},
  isbn          = {0-521-78451-4},
  mrclass       = {06-01 (68Q55)},
  mrnumber      = {1902334},
  mrreviewer    = {T. S. Blyth},
  doi           = {10.1017/CBO9780511809088},
  url           = {https://doi.org/10.1017/CBO9780511809088}
}

@InProceedings{   deligne_formulaire,
  author        = {Deligne, P.},
  title         = {Courbes elliptiques: formulaire d'apr\`es {J}. {T}ate},
  booktitle     = {Modular functions of one variable, {IV} ({P}roc.
                  {I}nternat. {S}ummer {S}chool, {U}niv. {A}ntwerp,
                  {A}ntwerp, 1972)},
  pages         = {53--73. Lecture Notes in Math., Vol. 476},
  year          = {1975},
  mrclass       = {14K15 (10D05)},
  mrnumber      = {0387292},
  mrreviewer    = {Jacques Velu}
}

@InProceedings{   demoura2015lean,
  author        = {de Moura, Leonardo and Kong, Soonho and Avigad, Jeremy and
                  van Doorn, Floris and von Raumer, Jakob},
  editor        = {Felty, Amy P. and Middeldorp, Aart},
  title         = {The Lean Theorem Prover (System Description)},
  booktitle     = {Automated Deduction - CADE-25},
  year          = {2015},
  publisher     = {Springer International Publishing},
  address       = {Cham},
  pages         = {378--388},
  isbn          = {978-3-319-21401-6}
}

@Article{         dold1958,
  author        = {Dold, Albrecht},
  title         = {Homology of symmetric products and other functors of
                  complexes},
  journal       = {Ann. of Math. (2)},
  fjournal      = {Annals of Mathematics. Second Series},
  volume        = {68},
  year          = {1958},
  pages         = {54--80},
  issn          = {0003-486X},
  mrclass       = {55.00},
  mrnumber      = {97057},
  mrreviewer    = {Sze-tsen Hu},
  doi           = {10.2307/1970043}
}

@Misc{            dupuis-lewis-macbeth2022,
  title         = {Formalized functional analysis with semilinear maps},
  author        = {Frédéric Dupuis and Robert Y. Lewis and Heather
                  Macbeth},
  year          = {2022},
  eprint        = {2202.05360},
  archiveprefix = {arXiv},
  primaryclass  = {cs.LO}
}

@Article{         dyckhoff_1992,
  author        = {Dyckhoff, Roy},
  title         = {Contraction-free sequent calculi for intuitionistic
                  logic},
  journal       = {Journal of Symbolic Logic},
  number        = {3},
  year          = {1992},
  pages         = {795–807},
  volume        = {57},
  publisher     = {Cambridge University Press},
  doi           = {10.2307/2275431}
}

@Book{            EinsiedlerWard2017,
  author        = {Einsiedler, Manfred and Ward, Thomas},
  title         = {Functional Analysis, Spectral Theory, and Applications},
  year          = 2017,
  publisher     = {Springer},
  doi           = {10.1007/978-3-319-58540-6}
}

@Book{            Eisenbud1995,
  title         = "Commutative algebra",
  author        = "Eisenbud, David",
  publisher     = "Springer",
  series        = "Graduate Texts in Mathematics",
  month         = mar,
  year          = 1995,
  address       = "New York, NY",
  language      = "en",
  isbn          = {978-0-387-94268-1},
  doi           = {10.1007/978-1-4612-5350-1}
}

@Book{            Elephant,
  title         = {Sketches of an Elephant – A Topos Theory Compendium},
  author        = {Peter Johnstone},
  year          = {2002},
  publisher     = {Oxford University Press}
}

@Book{            engel1997,
  title         = {Sperner theory},
  author        = {Engel, Konrad},
  publisher     = {Cambridge University Press},
  place         = {Cambridge},
  year          = {1997}
}

@Article{         erdosrenyisos,
  author        = {P. Erd\"os, A.R\'enyi, and V. S\'os},
  title         = {On a problem of graph theory},
  journal       = {Studia Sci. Math.},
  number        = {1},
  year          = {1966},
  pages         = {215--235},
  url           = {https://www.renyi.hu/~p_erdos/1966-06.pdf}
}

@Article{         etemadi_strong_law,
  author        = {Etemadi, Nasrollah},
  title         = {An elementary proof of the strong law of large numbers},
  journal       = {Z. Wahrsch. Verw. Gebiete},
  fjournal      = {Zeitschrift f\"{u}r Wahrscheinlichkeitstheorie und
                  Verwandte Gebiete},
  volume        = {55},
  year          = {1981},
  number        = {1},
  pages         = {119--122},
  issn          = {0044-3719},
  mrclass       = {60F15 (60B12)},
  mrnumber      = {606010},
  mrreviewer    = {Robert L. Taylor},
  doi           = {10.1007/BF01013465},
  url           = {https://doi.org/10.1007/BF01013465}
}

@Book{            Federer1996,
  author        = {Herbert Federer},
  title         = {Geometric Measure Theory},
  series        = {Classics in Mathematics},
  year          = {1996},
  publisher     = {Springer-Verlag Berlin Heidelberg},
  issn          = {1431-0821},
  doi           = {10.1007/978-3-642-62010-2},
  numpages      = {677}
}

@Article{         FennRourke1992,
  author        = {Fenn, Roger and Rourke, Colin},
  journal       = {Journal of Knot Theory and its Ramifications},
  title         = {Racks and links in codimension two},
  year          = {1992},
  issn          = {0218-2165},
  number        = {4},
  pages         = {343--406},
  volume        = {1},
  doi           = {10.1142/S0218216592000203},
  keywords      = {57M25 (57N10)},
  mrnumber      = {1194995}
}

@InProceedings{   flypitch_cpp,
  doi           = {10.1145/3372885.3373826},
  url           = {https://doi.org/10.1145/3372885.3373826},
  year          = {2020},
  month         = jan,
  publisher     = {{ACM}},
  author        = {Jesse Michael Han and Floris van Doorn},
  title         = {A formal proof of the independence of the continuum
                  hypothesis},
  booktitle     = {Proceedings of the 9th {ACM} {SIGPLAN} International
                  Conference on Certified Programs and Proofs}
}

@InProceedings{   flypitch_itp,
  author        = {Jesse Michael Han and Floris van Doorn},
  title         = {{A Formalization of Forcing and the Unprovability of the
                  Continuum Hypothesis}},
  booktitle     = {10th International Conference on Interactive Theorem
                  Proving (ITP 2019)},
  pages         = {19:1--19:19},
  series        = {Leibniz International Proceedings in Informatics
                  (LIPIcs)},
  isbn          = {978-3-95977-122-1},
  issn          = {1868-8969},
  year          = {2019},
  volume        = {141},
  editor        = {John Harrison and John O'Leary and Andrew Tolmach},
  publisher     = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address       = {Dagstuhl, Germany},
  url           = {http://drops.dagstuhl.de/opus/volltexte/2019/11074},
  urn           = {urn:nbn:de:0030-drops-110742},
  doi           = {10.4230/LIPIcs.ITP.2019.19},
  annote        = {Keywords: Interactive theorem proving, formal
                  verification, set theory, forcing, independence proofs,
                  continuum hypothesis, Boolean-valued models, Lean}
}

@Book{            fremlin_vol2,
  author        = {Fremlin, David H.},
  title         = {Measure theory. {V}ol. 2},
  note          = {Broad foundations, 2010 edition},
  publisher     = {Torres Fremlin, Colchester},
  year          = {2010},
  isbn          = {0-9538129-2-8}
}

@Book{            fremlin_vol4,
  author        = {Fremlin, David H.},
  title         = {Measure theory. {V}ol. 4},
  note          = {Topological Measure Spaces},
  publisher     = {Torres Fremlin, Colchester},
  year          = {2003}
}

@Book{            freyd1964abelian,
  title         = {Abelian categories},
  author        = {Freyd, Peter J},
  series        = {Harper's Series in Modern Mathematics},
  year          = {1964},
  publisher     = {Harper \& Row New York}
}

@Book{            friedmanscarr2005,
  author        = {Yaakov {Friedman}},
  title         = {{Physical applications of homogeneous balls. With the
                  assistance of Tzvi Scarr}},
  fjournal      = {{Progress in Mathematical Physics}},
  journal       = {{Prog. Math. Phys.}},
  issn          = {1544-9998},
  volume        = {40},
  isbn          = {0-8176-3339-1},
  pages         = {xxiv + 279},
  year          = {2005},
  publisher     = {Boston, MA: Birkh\"auser},
  language      = {English},
  msc2010       = {46-02 17C65 46L60 46G20 46L70 83A05},
  zbl           = {1080.46001}
}

@Book{            fuchs1963,
  author        = {Fuchs, L.},
  title         = {Partially ordered algebraic systems},
  publisher     = {Pergamon Press, Oxford-London-New York-Paris;
                  Addison-Wesley Publishing Co., Inc., Reading, Mass.-Palo
                  Alto, Calif.-London},
  year          = {1963},
  pages         = {ix+229},
  mrclass       = {06.00 (20.00)},
  mrnumber      = {0171864},
  mrreviewer    = {P. F. Conrad}
}

@InProceedings{   fuerer-lochbihler-schneider-traytel2020,
  author        = {Basil F{\"{u}}rer and Andreas Lochbihler and Joshua
                  Schneider and Dmitriy Traytel},
  editor        = {Nicolas Peltier and Viorica Sofronie{-}Stokkermans},
  title         = {Quotients of Bounded Natural Functors},
  booktitle     = {Automated Reasoning - 10th International Joint Conference,
                  {IJCAR} 2020, Paris, France, July 1-4, 2020, Proceedings,
                  Part {II}},
  series        = {Lecture Notes in Computer Science},
  volume        = {12167},
  pages         = {58--78},
  publisher     = {Springer},
  year          = {2020},
  url           = {https://doi.org/10.1007/978-3-030-51054-1\_4},
  doi           = {10.1007/978-3-030-51054-1\_4},
  timestamp     = {Mon, 06 Jul 2020 09:05:32 +0200},
  biburl        = {https://dblp.org/rec/conf/cade/FurerLST20.bib},
  bibsource     = {dblp computer science bibliography, https://dblp.org}
}

@Article{         furedi-loeb1994,
  author        = {Zolt\'an {F\"uredi} and Peter A. {Loeb}},
  journal       = {{Proc. Am. Math. Soc.}},
  title         = {{On the best constant for the Besicovitch covering
                  theorem}},
  year          = {1994},
  issn          = {0002-9939},
  number        = {4},
  pages         = {1063--1073},
  volume        = {121},
  doi           = {10.2307/2161215},
  fjournal      = {{Proceedings of the American Mathematical Society}},
  language      = {English},
  msc2010       = {28A75 05B40 51M16},
  publisher     = {American Mathematical Society (AMS), Providence, RI},
  zbl           = {0802.28002}
}

@Book{            gabriel-zisman-1967,
  author        = {Gabriel, P. and Zisman, M.},
  title         = {Calculus of fractions and homotopy theory},
  series        = {Ergebnisse der Mathematik und ihrer Grenzgebiete, Band
                  35},
  publisher     = {Springer-Verlag New York, Inc., New York},
  year          = {1967},
  pages         = {x+168}
}

@Article{         Gallagher1961,
  author        = {Gallagher, Patrick},
  title         = {Approximation by reduced fractions},
  journal       = {J. Math. Soc. Japan},
  fjournal      = {Journal of the Mathematical Society of Japan},
  volume        = {13},
  year          = {1961},
  pages         = {342--345},
  issn          = {0025-5645},
  mrclass       = {10.30},
  mrnumber      = {133297},
  mrreviewer    = {J. W. S. Cassels},
  doi           = {10.2969/jmsj/01340342},
  url           = {https://doi.org/10.2969/jmsj/01340342}
}

@InProceedings{   Gallier2011Notes,
  title         = {Notes on Differential Geometry and Lie Groups},
  author        = {J. Gallier and J. Quaintance},
  year          = {2011},
  url           = {https://www.cis.upenn.edu/~cis610/diffgeom-n.pdf}
}

@Unpublished{     gartnerMatousek,
  title         = {Cone Programming},
  author        = {B. G{\"{a}}rtner and J. Matousek},
  url           = {https://ti.inf.ethz.ch/ew/lehre/ApproxSDP09/notes/conelp.pdf}
}

@Article{         ghys87:groupes,
  author        = {Étienne Ghys},
  title         = {Groupes d'homéomorphismes du cercle et cohomologie
                  bornée},
  journal       = {Contemporary Mathematics},
  year          = 1987,
  volume        = 58,
  number        = {III},
  pages         = {81-106},
  doi           = {10.1090/conm/058.3/893858},
  language      = {french}
}

@Article{         gibbons2009,
  title         = {The essence of the Iterator pattern},
  volume        = {19},
  issn          = {0956-7968, 1469-7653},
  url           = {https://www.cambridge.org/core/product/identifier/S0956796809007291/type/journal_article},
  doi           = {10.1017/S0956796809007291},
  language      = {en},
  number        = {3-4},
  urldate       = {2021-10-24},
  journal       = {Journal of Functional Programming},
  author        = {Gibbons, Jeremy and Oliveira, BRUNO C. d. S.},
  month         = jul,
  year          = {2009},
  pages         = {377--402}
}

@Book{            GierzEtAl1980,
  author        = {Gierz, Gerhard and Hofmann, Karl Heinrich and Keimel,
                  Klaus and Lawson, Jimmie D. and Mislove, Michael W. and
                  Scott, Dana S.},
  title         = {A compendium of continuous lattices},
  publisher     = {Springer-Verlag, Berlin-New York},
  year          = {1980},
  pages         = {xx+371},
  isbn          = {3-540-10111-X},
  mrclass       = {06B30 (03G10 30G30 54H12)},
  mrnumber      = {614752},
  mrreviewer    = {James W. Lea, Jr.}
}

@Article{         gleason1958,
  author        = {Gleason, Andrew M.},
  title         = {Projective topological spaces},
  journal       = {Illinois J. Math.},
  fjournal      = {Illinois Journal of Mathematics},
  volume        = {2},
  year          = {1958},
  pages         = {482--489},
  issn          = {0019-2082},
  mrclass       = {54.00},
  mrnumber      = {121775},
  mrreviewer    = {Dana Scott},
  url           = {http://projecteuclid.org/euclid.ijm/1255454110}
}

@Book{            goerss-jardine-2009,
  author        = {Goerss, Paul G. and Jardine, John F.},
  title         = {Simplicial homotopy theory},
  series        = {Modern Birkh\"{a}user Classics},
  note          = {Reprint of the 1999 edition [MR1711612]},
  publisher     = {Birkh\"{a}user Verlag, Basel},
  year          = {2009},
  pages         = {xvi+510},
  isbn          = {978-3-0346-0188-7},
  mrclass       = {55U10 (18G55)},
  mrnumber      = {2840650},
  doi           = {10.1007/978-3-0346-0189-4}
}

@Book{            Gordon55,
  author        = {Russel A. Gordon},
  title         = {The integrals of Lebesgue, Denjoy, Perron, and Henstock},
  isbn          = {0-8218-3805-9},
  year          = {1955},
  series        = {Graduate Studies in Mathematics},
  volume        = 4,
  publisher     = {American Mathematical Society, Providence, R.I}
}

@Book{            gouvea1997,
  author        = {Gouv\^{e}a, Fernando Q.},
  title         = {{$p$}-adic numbers},
  series        = {Universitext},
  edition       = {Second},
  note          = {An introduction},
  publisher     = {Springer-Verlag, Berlin},
  year          = {1997},
  pages         = {vi+298},
  isbn          = {3-540-62911-4},
  mrclass       = {11S80 (11-01 12J25)},
  mrnumber      = {1488696},
  doi           = {10.1007/978-3-642-59058-0},
  url           = {https://doi.org/10.1007/978-3-642-59058-0}
}

@Book{            Gratzer2011,
  author        = {Gr{\"a}tzer, George},
  title         = {Lattice Theory: Foundation},
  year          = {2011},
  publisher     = {Springer, Basel},
  pages         = {xxx+614},
  isbn          = {978-3-0348-0018-1},
  doi           = {10.1007/978-3-0348-0018-1},
  mrnumber      = {2768581}
}

@Unpublished{     grinberg_clifford_2016,
  title         = {The {Clifford} algebra and the {Chevalley} map- a
                  computational approach (summary version 1)},
  url           = {http://mit.edu/~darij/www/algebra/chevalleys.pdf},
  author        = {Grinberg, D.},
  month         = jun,
  year          = {2016}
}

@Book{            gunter1992,
  title         = {Semantics of Programming Languages: Structures and
                  Techniques},
  isbn          = {0262570955},
  publisher     = {MIT Press},
  author        = {Gunter, Carl A.},
  year          = {1992}
}

@Article{         Gusakov2021,
  author        = {Alena Gusakov and Bhavik Mehta and Kyle A. Miller},
  title         = {Formalizing Hall's Marriage Theorem in Lean},
  eprint        = {2101.00127},
  eprintclass   = {math.CO},
  eprinttype    = {arXiv},
  keywords      = {math.CO, cs.LO, 05-04 (Primary) 05C70, 68R05 (Secondary)}
}

@Article{         Hall1935,
  author        = {P. Hall},
  journal       = {Journal of the London Mathematical Society},
  title         = {On Representatives of Subsets},
  year          = {1935},
  month         = {jan},
  number        = {1},
  pages         = {26--30},
  volume        = {s1-10},
  doi           = {10.1112/jlms/s1-10.37.26},
  publisher     = {Wiley}
}

@Book{            halmos1950measure,
  author        = {Halmos, Paul R},
  title         = {Measure theory},
  publisher     = {Springer-Verlag New York},
  year          = 1950,
  isbn          = {978-1-4684-9440-2},
  doi           = {10.1007/978-1-4684-9440-2}
}

@Book{            halmos2013measure,
  title         = {Measure theory},
  author        = {Halmos, Paul R},
  volume        = {18},
  year          = {1950},
  publisher     = {Springer},
  isbn          = {0-387-90088-8}
}

@Article{         Halpern1966,
  author        = {Halpern, James D.},
  journal       = {Proc. Amer. Math. Soc.},
  title         = {Bases in vector spaces and the axiom of choice},
  year          = {1966},
  issn          = {0002-9939},
  pages         = {670--673},
  volume        = {17},
  doi           = {10.2307/2035388},
  fjournal      = {Proceedings of the American Mathematical Society},
  mrclass       = {04.00},
  mrnumber      = {194340},
  mrreviewer    = {Ivan Singer}
}

@Book{            hancheolsenstormer1984,
  author        = {Harald {Hanche-Olsen} and Erling {St{\o}rmer}},
  title         = {{Jordan operator algebras}},
  fjournal      = {{Monographs and Studies in Mathematics}},
  journal       = {{Monogr. Stud. Math.}},
  volume        = {21},
  year          = {1984},
  publisher     = {Pitman, Boston, MA},
  language      = {English},
  msc2010       = {46L99 46L05 17C65 46-02},
  zbl           = {0561.46031}
}

@Book{            har77,
  author        = {Hartshorne, Robin},
  title         = {Algebraic geometry},
  note          = {Graduate Texts in Mathematics, No. 52},
  publisher     = {Springer-Verlag, New York-Heidelberg},
  year          = {1977},
  pages         = {xvi+496},
  isbn          = {0-387-90244-9},
  mrclass       = {14-01},
  mrnumber      = {0463157},
  mrreviewer    = {Robert Speiser}
}

@Book{            hardy2008introduction,
  title         = {An Introduction to the Theory of Numbers},
  author        = {Hardy, GH and Wright, EM and Heath-Brown, Roger and
                  Silverman, Joseph},
  year          = {2008},
  publisher     = {Oxford University Press}
}

@Book{            harmandwernerwerner1993,
  author        = {Peter {Harmand} and Dirk {Werner} and Wend {Werner}},
  title         = {{\(M\)-ideals in Banach spaces and Banach algebras}},
  fjournal      = {{Lecture Notes in Mathematics}},
  journal       = {{Lect. Notes Math.}},
  issn          = {0075-8434},
  volume        = {1547},
  isbn          = {3-540-56814-X},
  pages         = {viii + 387},
  year          = {1993},
  publisher     = {Berlin: Springer-Verlag},
  language      = {English},
  doi           = {10.1007/BFb0084355},
  msc2010       = {46B20 46B25 46B22 46-02 46B28},
  zbl           = {0789.46011}
}

@Book{            hartshorne61,
  author        = {Hartshorne, Robin},
  title         = {Local cohomology},
  series        = {Lecture Notes in Mathematics, No. 41},
  note          = {A seminar given by A. Grothendieck, Harvard University,
                  Fall, 1961},
  publisher     = {Springer-Verlag, Berlin-New York},
  year          = {1967},
  pages         = {vi+106},
  mrclass       = {14.55 (18.00)},
  mrnumber      = {0224620},
  mrreviewer    = {F. Oort}
}

@Article{         Haze09,
  title         = {Witt vectors. Part 1},
  isbn          = {9780444532572},
  issn          = {1570-7954},
  url           = {http://dx.doi.org/10.1016/S1570-7954(08)00207-6},
  doi           = {10.1016/s1570-7954(08)00207-6},
  journal       = {Handbook of Algebra},
  publisher     = {Elsevier},
  author        = {Hazewinkel, Michiel},
  year          = {2009},
  pages         = {319–472}
}

@Article{         Higman52,
  author        = {Higman, Graham},
  title         = {Ordering by Divisibility in Abstract Algebras},
  journal       = {Proceedings of the London Mathematical Society},
  volume        = {s3-2},
  number        = {1},
  pages         = {326-336},
  doi           = {https://doi.org/10.1112/plms/s3-2.1.326},
  year          = {1952}
}

@Unpublished{     hochsterunpublished,
  title         = {Local cohomology},
  author        = {Hochster, Mel},
  url           = {https://dept.math.lsa.umich.edu/~hochster/615W11/loc.pdf}
}

@Book{            Hodges97,
  author        = {Hodges, Wilfrid},
  title         = {A Shorter Model Theory},
  year          = {1997},
  isbn          = {0521587131},
  publisher     = {Cambridge University Press},
  address       = {USA}
}

@Book{            Hofstadter-1979,
  author        = "Douglas R Hofstadter",
  title         = "{{G}ödel, {E}scher, {B}ach: an eternal golden braid}",
  publisher     = "Basic Books",
  address       = "New York, NY",
  series        = "Penguin books",
  year          = "1979"
}

@Misc{            howard,
  title         = {Second Order Elliptic PDE: The Lax-Milgram Theorem},
  url           = {https://www.math.tamu.edu/~phoward/m612/s20/elliptic2.pdf},
  journal       = {M612: Partial Differential Equations},
  author        = {Howard, Peter}
}

@Book{            HubbardWest-ode,
  author        = {John H. Hubbard and Beverly H. West},
  title         = {Differential Equations: A Dynamical Systems Approach},
  subtitle      = {Ordinary Differential Equations},
  year          = {1991},
  publisher     = {Springer},
  location      = {New York},
  volume        = {5},
  isbn          = {978-1-4612-8693-6},
  doi           = {10.1007/978-1-4612-4192-8},
  pages         = {XX, 350}
}

@Article{         huneke2002,
  author        = {Huneke, Craig},
  title         = {The Friendship Theorem},
  publisher     = {Mathematical Association of America},
  year          = {2002},
  pages         = {192--194},
  journal       = {The American Mathematical Monthly},
  issn          = {00029890, 19300972},
  volume        = {109},
  number        = {2},
  doi           = {10.1080/00029890.2002.11919853},
  url           = {https://doi.org/10.1080/00029890.2002.11919853}
}

@InProceedings{   hyman1973,
  author        = "Bass, Hyman",
  editor        = "Bass, Hyman",
  title         = "Unitary algebraic K-theory",
  booktitle     = "Hermitian K-Theory and Geometric Applications",
  year          = "1973",
  publisher     = "Springer Berlin Heidelberg",
  address       = "Berlin, Heidelberg",
  pages         = "57--265",
  isbn          = "978-3-540-37773-3"
}

@Book{            iordanescu2003,
  author        = {Radu {Iord\u{a}nescu}},
  title         = {{Jordan structures in geometry and physics. With an
                  appendix on Jordan structures in analysis}},
  isbn          = {973-27-0956-1},
  pages         = {201},
  year          = {2003},
  publisher     = {Bucharest: Editura Academiei Rom\^ane},
  language      = {English},
  msc2010       = {17C50 17-02 17C65 32M15 35Q58 51A35 53C35 46H70 46K70
                  81R12 81R50},
  zbl           = {1073.17014}
}

@Book{            IrelandRosen1990,
  author        = {Ireland, Kenneth and Rosen, Michael},
  title         = {A classical introduction to modern number theory},
  series        = {Graduate Texts in Mathematics},
  volume        = {84},
  edition       = {Second},
  publisher     = {Springer-Verlag, New York},
  year          = {1990},
  pages         = {xiv+389},
  isbn          = {0-387-97329-X},
  doi           = {10.1007/978-1-4757-2103-4},
  url           = {https://doi.org/10.1007/978-1-4757-2103-4}
}

@Book{            iyengaretal07,
  author        = {Iyengar, Srikanth B. and Leuschke, Graham J. and Leykin,
                  Anton and Miller, Claudia and Miller, Ezra and Singh,
                  Anurag K. and Walther, Uli},
  title         = {Twenty-four hours of local cohomology},
  series        = {Graduate Studies in Mathematics},
  volume        = {87},
  publisher     = {American Mathematical Society, Providence, RI},
  year          = {2007},
  pages         = {xviii+282},
  isbn          = {978-0-8218-4126-6},
  mrclass       = {13D45 (14B15 55N30)},
  doi           = {10.1090/gsm/087},
  url           = {https://doi-org.www2.lib.ku.edu/10.1090/gsm/087}
}

@Article{         izhakian2016,
  title         = {Supertropical quadratic forms I},
  journal       = {Journal of Pure and Applied Algebra},
  volume        = {220},
  number        = {1},
  pages         = {61-93},
  year          = {2016},
  issn          = {0022-4049},
  doi           = {10.1016/j.jpaa.2015.05.043},
  url           = {https://www.sciencedirect.com/science/article/pii/S0022404915001589},
  author        = {Zur Izhakian and Manfred Knebusch and Louis Rowen}
}

@Book{            Jacobson1956,
  author        = {Jacobson, Nathan},
  title         = {Structure of rings},
  fseries       = {Colloquium Publications. American Mathematical Society},
  series        = {Colloq. Publ., Am. Math. Soc.},
  issn          = {0065-9258},
  volume        = {37},
  year          = {1956},
  publisher     = {American Mathematical Society (AMS), Providence, RI},
  language      = {English},
  keywords      = {16-02},
  zbmath        = {3121681},
  zbl           = {0073.02002}
}

@Book{            james1999,
  author        = {James, Ioan},
  title         = {Topologies and uniformities},
  series        = {Springer Undergraduate Mathematics Series},
  note          = {Revised version of {{\i}t Topological and uniform spaces}
                  [Springer, New York, 1987; MR0884154 (89b:54001)]},
  publisher     = {Springer-Verlag London, Ltd., London},
  year          = {1999},
  pages         = {xvi+230},
  isbn          = {1-85233-061-9},
  mrclass       = {54-01 (54A05 54E15)},
  mrnumber      = {1687407},
  mrreviewer    = {Hans-Peter A. K\"{u}nzi},
  doi           = {10.1007/978-1-4471-3994-2},
  url           = {https://doi.org/10.1007/978-1-4471-3994-2}
}

@Article{         Jordan1935,
  title         = "On inner products in linear, metric spaces",
  author        = "Jordan, P. and von Neumann, J.",
  fjournal      = {{Annals of Mathematics}},
  journal       = "Ann. Math.",
  volume        = 36,
  number        = 3,
  pages         = "719-723",
  month         = jul,
  year          = 1935,
  url           = "http://www.mathematik.uni-muenchen.de/~michel/jordan-von_neumann_-_parallelogram_identity.pdf",
  doi           = {10.2307/1968653}
}

@Article{         joyal1977,
  author        = {André Joyal},
  title         = {Remarques sur la théorie des jeux à deux personnes},
  journal       = {Gazette des Sciences Mathematiques du Québec},
  volume        = {1},
  number        = {4},
  pages         = {46--52},
  year          = {1977},
  note          = {(English translation at
                  https://bosker.files.wordpress.com/2010/12/joyal-games.pdf)}
}

@Misc{            Joyal_Street,
  title         = {Braided monoidal categories},
  author        = {Andr{\'e} Joyal and Ross H. Street},
  year          = {1986},
  note          = {Mathematics Reports 860081, Macquarie University},
  url           = {http://maths.mq.edu.au/~street/JS1.pdf}
}

@Article{         Joyce1982,
  author        = {David Joyce},
  title         = {A classifying invariant of knots, the knot quandle},
  journal       = {Journal of Pure and Applied Algebra},
  year          = {1982},
  volume        = {23},
  number        = {1},
  month         = {1},
  pages         = {37--65},
  doi           = {10.1016/0022-4049(82)90077-9},
  publisher     = {Elsevier {BV}}
}

@Book{            kallenberg2021,
  author        = {Olav Kallenberg},
  title         = {Foundations of modern probability},
  series        = {Probability Theory and Stochastic Modelling},
  volume        = {99},
  publisher     = {Springer Nature Switzerland},
  edition       = {Third Edition},
  year          = {2021},
  pages         = {193},
  isbn          = {978-3-030-61870-4; 978-3-030-61871-1},
  doi           = {10.1007/978-3-030-61871-1},
  url           = {https://doi.org/10.1007/978-3-030-61871-1}
}

@Book{            katz_mazur,
  author        = {Katz, Nicholas M. and Mazur, Barry},
  title         = {Arithmetic moduli of elliptic curves},
  series        = {Annals of Mathematics Studies},
  volume        = {108},
  publisher     = {Princeton University Press, Princeton, NJ},
  year          = {1985},
  pages         = {xiv+514},
  isbn          = {0-691-08349-5; 0-691-08352-5},
  mrclass       = {11G05 (11F11 14G25 14K15)},
  mrnumber      = {772569},
  mrreviewer    = {Kenneth A. Ribet},
  doi           = {10.1515/9781400881710},
  url           = {https://doi.org/10.1515/9781400881710}
}

@Book{            kechris1995,
  author        = {Kechris, Alexander S.},
  title         = {Classical descriptive set theory},
  series        = {Graduate Texts in Mathematics},
  volume        = {156},
  publisher     = {Springer-Verlag, New York},
  year          = {1995},
  pages         = {xviii+402},
  isbn          = {0-387-94374-9},
  mrclass       = {03E15 (03-01 03-02 04A15 28A05 54H05 90D44)},
  mrnumber      = {1321597},
  mrreviewer    = {Jakub Jasi\'{n}ski},
  doi           = {10.1007/978-1-4612-4190-4},
  url           = {https://doi.org/10.1007/978-1-4612-4190-4}
}

@Article{         kelleyVaught1953,
  author        = {Kelley, J. L. and Vaught, R. L.},
  title         = {The positive cone in {Banach} algebras},
  journal       = {Trans. Am. Math. Soc.},
  issn          = {0002-9947},
  volume        = {74},
  pages         = {44--55},
  year          = {1953},
  language      = {English},
  doi           = {10.2307/1990847}
}

@Article{         kleiman1979,
  author        = {Kleiman, Steven Lawrence},
  title         = {Misconceptions about {$K\_X$}},
  journal       = {Enseign. Math. (2)},
  volume        = {25},
  year          = {1979},
  number        = {3-4},
  pages         = {203--206},
  url           = {http://dx.doi.org/10.5169/seals-50379}
}

@Article{         kleitman1966,
  author        = {Kleitman, D. J.},
  title         = {Families of non-disjoint subsets},
  journal       = {J. Comb. Theory},
  fjournal      = {Journal of Combinatorial Theory},
  issn          = {0097-3165},
  volume        = {1},
  year          = {1966},
  pages         = {153--155},
  language      = {English},
  doi           = {10.1016/S0021-9800(66)80012-1},
  zbl           = {0141.00801}
}

@Article{         KoukoulopoulosMaynard2020,
  author        = {Koukoulopoulos, Dimitris and Maynard, James},
  title         = {On the {D}uffin-{S}chaeffer conjecture},
  journal       = {Ann. of Math. (2)},
  fjournal      = {Annals of Mathematics. Second Series},
  volume        = {192},
  year          = {2020},
  number        = {1},
  pages         = {251--307},
  issn          = {0003-486X},
  mrclass       = {11J83 (05C40)},
  mrnumber      = {4125453},
  mrreviewer    = {Sam Chow},
  doi           = {10.4007/annals.2020.192.1.5},
  url           = {https://doi.org/10.4007/annals.2020.192.1.5}
}

@Article{         kozen1994,
  title         = {A Completeness Theorem for Kleene Algebras and the Algebra
                  of Regular Events},
  journal       = {Information and Computation},
  volume        = {110},
  number        = {2},
  pages         = {366-390},
  year          = {1994},
  issn          = {0890-5401},
  doi           = {https://doi.org/10.1006/inco.1994.1037},
  url           = {https://www.sciencedirect.com/science/article/pii/S0890540184710376},
  author        = {D. Kozen},
  abstract      = {We give a finitary axiomatization of the algebra of
                  regular events involving only equations and equational
                  implications. Unlike Salomaa′s axiomatizations, the
                  axiomatization given here is sound for all interpretations
                  over Kleene algebras.}
}

@Article{         lazarus1973,
  author        = {Michel Lazarus},
  title         = {Les familles libres maximales d'un module ont-elles le
                  meme cardinal?},
  journal       = {Pub. Sem. Math. Rennes},
  volume        = {4},
  year          = {1973},
  pages         = {1--12},
  url           = {http://www.numdam.org/article/PSMIR_1973___4_A4_0.pdf}
}

@InProceedings{   lewis2019,
  author        = {Lewis, Robert Y.},
  title         = {A Formal Proof of {H}ensel's Lemma over the {$p$}-adic
                  Integers},
  booktitle     = {Proceedings of the 8th ACM SIGPLAN International
                  Conference on Certified Programs and Proofs},
  series        = {CPP 2019},
  year          = {2019},
  isbn          = {978-1-4503-6222-1},
  location      = {Cascais, Portugal},
  pages         = {15--26},
  numpages      = {12},
  url           = {http://doi.acm.org/10.1145/3293880.3294089},
  doi           = {10.1145/3293880.3294089},
  acmid         = {3294089},
  publisher     = {ACM},
  address       = {New York, NY, USA},
  keywords      = {Hensel's lemma, Lean, formal proof, p-adic}
}

@Book{            LurieSAG,
  title         = {Spectral Algebraic Geometry},
  author        = {Jacob Lurie},
  url           = {https://www.math.ias.edu/~lurie/papers/SAG-rootfile.pdf},
  year          = {last updated 2018}
}

@Article{         manin1963,
  author        = {Manin, Ju. I.},
  title         = {Theory of commutative formal groups over fields of finite
                  characteristic},
  journal       = {Uspehi Mat. Nauk},
  fjournal      = {Akademiya Nauk SSSR i Moskovskoe Matematicheskoe
                  Obshchestvo. Uspekhi Matematicheskikh Nauk},
  volume        = {18},
  year          = {1963},
  number        = {6 (114)},
  pages         = {3--90},
  issn          = {0042-1316},
  mrclass       = {14.50 (14.49)},
  mrnumber      = {0157972},
  mrreviewer    = {E. C. Dade}
}

@Book{            marcus1977number,
  title         = {Number fields},
  author        = {Marcus, Daniel A and Sacco, Emanuele},
  volume        = {2},
  year          = {1977},
  publisher     = {Springer}
}

@Article{         markowsky1976,
  title         = {Chain-complete posets and directed sets with
                  applications},
  volume        = {6},
  doi           = {10.1007/bf02485815},
  number        = {1},
  journal       = {Algebra Universalis},
  author        = {Markowsky, George},
  year          = {1976},
  month         = {Dec},
  pages         = {53-68}
}

@InProceedings{   mathlib2020,
  author        = {The mathlib Community},
  title         = {The Lean Mathematical Library},
  year          = {2020},
  isbn          = {9781450370974},
  publisher     = {Association for Computing Machinery},
  address       = {New York, NY, USA},
  url           = {https://doi.org/10.1145/3372885.3373824},
  doi           = {10.1145/3372885.3373824},
  booktitle     = {Proceedings of the 9th ACM SIGPLAN International
                  Conference on Certified Programs and Proofs},
  pages         = {367-381},
  numpages      = {15},
  keywords      = {formal proof, formal library, Lean, mathlib},
  location      = {New Orleans, LA, USA},
  series        = {CPP 2020}
}

@InProceedings{   mcbride1996,
  title         = {Inverting inductively defined relations in {LEGO}},
  author        = {McBride, Conor},
  booktitle     = {International Workshop on Types for Proofs and Programs},
  pages         = {236--253},
  year          = {1996},
  organization  = {Springer}
}

@Book{            mccrimmon2004,
  author        = {Kevin {McCrimmon}},
  title         = {{A taste of Jordan algebras}},
  fjournal      = {{Universitext}},
  journal       = {{Universitext}},
  issn          = {0172-5939},
  isbn          = {0-387-95447-3},
  pages         = {xxvi + 562},
  year          = {2004},
  publisher     = {New York, NY: Springer},
  language      = {English},
  doi           = {10.1007/b97489},
  msc2010       = {17-01 17Cxx},
  zbl           = {1044.17001}
}

@Misc{            melikhov2011,
  title         = {Metrizable uniform spaces},
  author        = {Sergey A. Melikhov},
  year          = {2011},
  eprint        = {1106.3249},
  archiveprefix = {arXiv},
  primaryclass  = {math.GT}
}

@Book{            MeyerNieberg1991,
  author        = {Meyer-Nieberg, Peter},
  title         = {Banach lattices},
  series        = {Universitext},
  publisher     = {Springer-Verlag, Berlin},
  year          = {1991},
  pages         = {xvi+395},
  isbn          = {3-540-54201-9},
  mrclass       = {46B42 (46A40 47B60)},
  mrnumber      = {1128093},
  mrreviewer    = {Yu. A. Abramovich},
  doi           = {10.1007/978-3-642-76724-1},
  url           = {https://doi.org/10.1007/978-3-642-76724-1}
}

@Book{            miraglia2006introduction,
  title         = {An Introduction to Partially Ordered Structures and
                  Sheaves},
  author        = {Miraglia, F.},
  isbn          = {9788876990359},
  series        = {Contemporary logic},
  year          = {2006},
  publisher     = {Polimetrica}
}

@Book{            MM92,
  title         = {Sheaves in geometry and logic: A first introduction to
                  topos theory},
  author        = {MacLane, Saunders and Moerdijk, Ieke},
  year          = {1992},
  publisher     = {Springer Science \& Business Media}
}

@Article{         MR0236876,
  title         = {A new proof that metric spaces are paracompact},
  author        = {Mary Ellen Rudin},
  year          = 1969,
  journal       = {Proc. Amer. Math. Soc.},
  volume        = {20},
  pages         = {603},
  mrnumber      = {0236876},
  doi           = {10.1090/S0002-9939-1969-0236876-3}
}

@Book{            MR0302656,
  author        = {Demazure, Michel and Gabriel, Pierre},
  title         = {Groupes alg\'{e}briques. {T}ome {I}: {G}\'{e}om\'{e}trie
                  alg\'{e}brique, g\'{e}n\'{e}ralit\'{e}s, groupes commutatifs},
  note          = {Avec un appendice {{\i}t Corps de classes local} par
                  Michiel Hazewinkel},
  publisher     = {Masson \& Cie, \'{E}diteur, Paris; North-Holland
                  Publishing Co., Amsterdam},
  year          = {1970},
  pages         = {xxvi+700},
  mrclass       = {14L15 (20G35)},
  mrnumber      = {0302656},
  mrreviewer    = {J.-E. Bertin}
}

@Article{         MR1167694,
  author        = {Blass, Andreas},
  title         = {A game semantics for linear logic},
  journal       = {Ann. Pure Appl. Logic},
  fjournal      = {Annals of Pure and Applied Logic},
  volume        = {56},
  year          = {1992},
  number        = {1-3},
  pages         = {183--220},
  issn          = {0168-0072},
  mrclass       = {03B70 (68Q55)},
  mrnumber      = {1167694},
  mrreviewer    = {Fangmin Song},
  doi           = {10.1016/0168-0072(92)90073-9},
  url           = {https://doi.org/10.1016/0168-0072(92)90073-9}
}

@Book{            MR1237403,
  author        = {Lidl, R. and Mullen, G. L. and Turnwald, G.},
  title         = {Dickson polynomials},
  series        = {Pitman Monographs and Surveys in Pure and Applied
                  Mathematics},
  volume        = {65},
  publisher     = {Longman Scientific \& Technical, Harlow; copublished in
                  the United States with John Wiley \& Sons, Inc., New York},
  year          = {1993},
  pages         = {vi+207},
  isbn          = {0-582-09119-5},
  mrclass       = {11T06 (12E05 13B25 33C80 94A60)},
  mrnumber      = {1237403},
  mrreviewer    = {S. D. Cohen}
}

@Article{         MR25465,
  author        = {van der Waerden, B. L.},
  title         = {Free products of groups},
  journal       = {Amer. J. Math.},
  fjournal      = {American Journal of Mathematics},
  volume        = {70},
  year          = {1948},
  pages         = {527--528},
  issn          = {0002-9327},
  mrclass       = {20.0X},
  mrnumber      = {25465},
  mrreviewer    = {P. Hall},
  doi           = {10.2307/2372196},
  url           = {https://doi.org/10.2307/2372196}
}

@Article{         MR317916,
  author        = {Davis, Martin},
  title         = {Hilbert's tenth problem is unsolvable},
  journal       = {Amer. Math. Monthly},
  fjournal      = {American Mathematical Monthly},
  volume        = {80},
  year          = {1973},
  pages         = {233--269},
  issn          = {0002-9890},
  mrclass       = {02G05 (10B99 10N05)},
  mrnumber      = {317916},
  mrreviewer    = {R. L. Goodstein},
  doi           = {10.2307/2318447},
  url           = {https://doi.org/10.2307/2318447}
}

@Article{         MR32592,
  author        = {Motzkin, Th.},
  title         = {The {E}uclidean algorithm},
  journal       = {Bull. Amer. Math. Soc.},
  fjournal      = {Bulletin of the American Mathematical Society},
  volume        = {55},
  year          = {1949},
  pages         = {1142--1146},
  issn          = {0002-9904},
  mrclass       = {09.1X},
  mrnumber      = {32592},
  mrreviewer    = {B. N. Moyls},
  doi           = {10.1090/S0002-9904-1949-09344-8},
  url           = {https://doi.org/10.1090/S0002-9904-1949-09344-8}
}

@Article{         MR3790629,
  author        = {Bell, J. S.},
  title         = {On the {E}instein {P}odolsky {R}osen paradox},
  journal       = {Phys. Phys. Fiz.},
  fjournal      = {Physics Physique Fizika},
  volume        = {1},
  year          = {1964},
  number        = {3},
  pages         = {195--200},
  issn          = {0554-128X},
  mrclass       = {DML},
  mrnumber      = {3790629},
  doi           = {10.1103/PhysicsPhysiqueFizika.1.195},
  url           = {https://doi.org/10.1103/PhysicsPhysiqueFizika.1.195}
}

@Article{         MR399081,
  author        = {Hiblot, Jean-Jacques},
  title         = {Des anneaux euclidiens dont le plus petit algorithme n'est
                  pas \`a valeurs finies},
  journal       = {C. R. Acad. Sci. Paris S\'{e}r. A-B},
  fjournal      = {Comptes Rendus Hebdomadaires des S\'{e}ances de
                  l'Acad\'{e}mie des Sciences. S\'{e}ries A et B},
  volume        = {281},
  year          = {1975},
  number        = {12},
  pages         = {Ai, A411--A414},
  issn          = {0151-0509},
  mrclass       = {13F15 (12A20)},
  mrnumber      = {399081},
  mrreviewer    = {N. Sankaran}
}

@InCollection{    MR541021,
  author        = {Nagata, Masayoshi},
  title         = {On {E}uclid algorithm},
  booktitle     = {C. {P}. {R}amanujam---a tribute},
  series        = {Tata Inst. Fund. Res. Studies in Math.},
  volume        = {8},
  pages         = {175--186},
  publisher     = {Springer, Berlin-New York},
  year          = {1978},
  mrclass       = {13F07},
  mrnumber      = {541021},
  mrreviewer    = {Daniel Lazard}
}

@Article{         MR577178,
  author        = {Cirel\cprime son, B. S.},
  title         = {Quantum generalizations of {B}ell's inequality},
  journal       = {Lett. Math. Phys.},
  fjournal      = {Letters in Mathematical Physics. A Journal for the Rapid
                  Dissemination of Short Contributions in the Field of
                  Mathematical Physics},
  volume        = {4},
  year          = {1980},
  number        = {2},
  pages         = {93--100},
  issn          = {0377-9017},
  mrclass       = {81B05},
  mrnumber      = {577178},
  doi           = {10.1007/BF00417500},
  url           = {https://doi.org/10.1007/BF00417500}
}

@Article{         Nash-Williams63,
  title         = {On well-quasi-ordering finite trees},
  volume        = {59},
  doi           = {10.1017/S0305004100003844},
  number        = {4},
  journal       = {Mathematical Proceedings of the Cambridge Philosophical
                  Society},
  publisher     = {Cambridge University Press},
  author        = {Nash-Williams, C. St. J. A.},
  year          = {1963},
  pages         = {833–835}
}

@Book{            Neukirch1992,
  author        = {Neukirch, J.},
  title         = {Algebraic number theory},
  series        = {Fundamental Principles of Mathematical Sciences},
  volume        = {322},
  note          = {Translated from the 1992 German original and with a note
                  by Norbert Schappacher, With a foreword by G. Harder},
  publisher     = {Springer-Verlag, Berlin},
  year          = {1999},
  pages         = {xviii+571},
  isbn          = {3-540-65399-6},
  doi           = {10.1007/978-3-662-03983-0}
}

@Article{         orosi2018faulhaber,
  author        = {Greg {Orosi}},
  title         = {{A simple derivation of Faulhaber's formula}},
  fjournal      = {{Applied Mathematics E-Notes}},
  journal       = {{Appl. Math. E-Notes}},
  issn          = {1607-2510/e},
  volume        = {18},
  pages         = {124--126},
  year          = {2018},
  publisher     = {Tsing Hua University, Department of Mathematics, Hsinchu},
  language      = {English},
  msc2010       = {41A58 30K05},
  zbl           = {1411.41023}
}

@InCollection{    petridis2014,
  author        = {Petridis, G.},
  title         = {The {Pl{\"u}nnecke}-{Ruzsa} inequality: an overview},
  booktitle     = {Combinatorial and additive number theory. Selected papers
                  based on the presentations at the conferences CANT 2011 and
                  2012, New York, NY, USA, May 2011 and May 2012},
  isbn          = {978-1-4939-1600-9; 978-1-4939-1601-6},
  pages         = {229--241},
  year          = {2014},
  publisher     = {New York, NY: Springer},
  language      = {English},
  doi           = {10.1007/978-1-4939-1601-6_16},
  keywords      = {11B30},
  zblath        = {6463830},
  zbl           = {1371.11029}
}

@Article{         phillips1940,
  author        = {Phillips, Ralph S.},
  title         = {Integration in a convex linear topological space},
  journal       = {Trans. Amer. Math. Soc.},
  fjournal      = {Transactions of the American Mathematical Society},
  volume        = {47},
  year          = {1940},
  pages         = {114--145},
  issn          = {0002-9947},
  mrclass       = {46.3X},
  mrnumber      = {2707},
  mrreviewer    = {B. J. Pettis},
  doi           = {10.2307/1990004},
  url           = {https://doi.org/10.2307/1990004}
}

@Misc{            ponton2020chebyshev,
  title         = {Roots of {C}hebyshev polynomials: a purely algebraic
                  approach},
  author        = {Lionel Ponton},
  year          = {2020},
  eprint        = {2008.03575},
  archiveprefix = {arXiv},
  primaryclass  = {math.NT}
}

@Misc{            pöschel2017siegelsternberg,
  title         = {On the Siegel-Sternberg linearization theorem},
  author        = {Jürgen Pöschel},
  year          = {2017},
  eprint        = {1702.03691},
  archiveprefix = {arXiv},
  primaryclass  = {math.DS}
}

@Book{            riehl2017,
  author        = {Riehl, Emily},
  title         = {Category theory in context},
  publisher     = {Dover Publications},
  year          = {2017},
  isbn          = {048680903X},
  url           = {http://www.math.jhu.edu/~eriehl/context.pdf}
}

@Misc{            RisingSea,
  author        = "Vakil, Ravi",
  title         = "{The Rising Sea: Foundations Of Algebraic Geometry Notes}",
  url           = "https://math.stanford.edu/~vakil/216blog/"
}

@Book{            rudin2006real,
  title         = {Real and Complex Analysis},
  author        = {Rudin, Walter},
  year          = {1987},
  publisher     = {McGraw-Hill Book Company},
  edition       = {Third Edition},
  isbn          = {0-07-100276-6}
}

@Article{         salwinski2018,
  author        = {Salwinski, David},
  title         = {Euler's sine product formula: an elementary proof},
  journal       = {College Math. J.},
  fjournal      = {The College Mathematics Journal},
  volume        = {49},
  year          = {2018},
  number        = {2},
  pages         = {126--135},
  issn          = {0746-8342},
  mrclass       = {26A06 (00A05)},
  mrnumber      = {3766700},
  doi           = {10.1080/07468342.2018.1419703}
}

@Book{            samuel1967,
  author        = {Samuel, Pierre},
  title         = {Th\'{e}orie alg\'{e}brique des nombres},
  publisher     = {Hermann, Paris},
  year          = {1967},
  pages         = {130},
  mrclass       = {10.65 (12.00)},
  mrnumber      = {0215808}
}

@Book{            schaefer1966,
  title         = {Topological Vector Spaces},
  author        = {Schaefer, H.H.},
  lccn          = {65024692},
  series        = {Graduate Texts in Mathematics},
  year          = {1966},
  publisher     = {Macmillan}
}

@Misc{            schleicher_stoll,
  author        = {Dierk Schleicher and Michael Stoll},
  title         = {An introduction to {C}onway's games and numbers},
  url           = {http://www.cs.cmu.edu/afs/cs/academic/class/15859-s05/www/lecture-notes/comb-games-notes.pdf}
}

@Misc{            scholze2011perfectoid,
  title         = {Perfectoid spaces},
  author        = {Peter Scholze},
  year          = {2011},
  eprint        = {1111.4914},
  archiveprefix = {arXiv},
  primaryclass  = {math.AG}
}

@Book{            seligman1967,
  author        = {Seligman, G. B.},
  title         = {Modular {L}ie algebras},
  series        = {Ergebnisse der Mathematik und ihrer Grenzgebiete, Band
                  40},
  publisher     = {Springer-Verlag New York, Inc., New York},
  year          = {1967},
  pages         = {ix+165},
  mrclass       = {17.30 (22.00)},
  mrnumber      = {0245627},
  mrreviewer    = {R. E. Block}
}

@Article{         serre1951,
  author        = {Serre, Jean-Pierre},
  title         = {Homologie singuli\`ere des espaces fibr\'{e}s.
                  {A}pplications},
  journal       = {Ann. of Math. (2)},
  year          = {1951},
  volume        = {54},
  pages         = {425--505},
  issn          = {0003-486X},
  doi           = {10.2307/1969485},
  fjournal      = {Annals of Mathematics. Second Series},
  mrclass       = {56.0X},
  mrnumber      = {0045386},
  mrreviewer    = {W. S. Massey}
}

@Book{            serre1965,
  author        = {Serre, Jean-Pierre},
  title         = {Complex semisimple {L}ie algebras},
  note          = {Translated from the French by G. A. Jones},
  publisher     = {Springer-Verlag, New York},
  year          = {1987},
  pages         = {x+74},
  isbn          = {0-387-96569-6},
  mrclass       = {17-01 (17B20)},
  mrnumber      = {914496},
  doi           = {10.1007/978-1-4757-3910-7}
}

@Book{            silverman2009,
  author        = {Silverman, Joseph},
  publisher     = {Springer New York, NY},
  series        = {Graduate Texts in Mathematics},
  title         = {The Arithmetic of Elliptic Curves},
  year          = {2009}
}

@Book{            simon2011,
  author        = {Simon, Barry},
  title         = {Convexity: An Analytic Viewpoint},
  year          = {2011},
  series        = {Cambridge Tracts in Mathematics},
  publisher     = {Cambridge University Press},
  place         = {Cambridge},
  doi           = {10.1017/CBO9780511910135},
  collection    = {Cambridge Tracts in Mathematics}
}

@Article{         skoda2006,
  author        = {{\v{S}}koda, Zoran},
  title         = {Noncommutative localization in noncommutative geometry},
  journal       = {London Math. Soc. Lecture Note Series},
  fjournal      = {London Mathematical Society Lecture Note Series},
  volume        = {330},
  pages         = {220--313},
  year          = {2006},
  url           = {https://doi.org/10.48550/arXiv.math/0403276}
}

@Book{            soare1987,
  author        = {Soare, Robert I.},
  title         = {Recursively enumerable sets and degrees},
  series        = {Perspectives in Mathematical Logic},
  note          = {A study of computable functions and computably generated
                  sets},
  publisher     = {Springer-Verlag, Berlin},
  year          = {1987},
  pages         = {xviii+437},
  isbn          = {3-540-15299-7},
  mrclass       = {03-02 (03D20 03D25 03D30)},
  mrnumber      = {882921},
  mrreviewer    = {Peter G. Hinman},
  doi           = {10.1007/978-3-662-02460-7}
}

@InProceedings{   srl_itp,
  author        = {Dillies, Ya\"{e}l and Mehta, Bhavik},
  title         = {{Formalising Szemer\'{e}di’s Regularity Lemma in Lean}},
  booktitle     = {13th International Conference on Interactive Theorem
                  Proving (ITP 2022)},
  pages         = {9:1--9:19},
  series        = {Leibniz International Proceedings in Informatics
                  (LIPIcs)},
  isbn          = {978-3-95977-252-5},
  issn          = {1868-8969},
  year          = {2022},
  volume        = {237},
  editor        = {Andronick, June and de Moura, Leonardo},
  publisher     = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address       = {Dagstuhl, Germany},
  url           = {https://drops.dagstuhl.de/opus/volltexte/2022/16718},
  urn           = {urn:nbn:de:0030-drops-167185},
  doi           = {10.4230/LIPIcs.ITP.2022.9},
  annote        = {Keywords: Lean, formalisation, formal proof, graph theory,
                  combinatorics, additive combinatorics, Szemer\'{e}di’s
                  Regularity Lemma, Roth’s Theorem}
}

@Book{            stanley2012,
  author        = {Stanley, Richard P.},
  title         = {Enumerative combinatorics},
  place         = {Cambridge},
  publisher     = {Cambridge Univ. Press},
  year          = {2012}
}

@Book{            stern2009,
  author        = {Stern, Manfred},
  title         = {Semimodular lattices. {Theory} and applications},
  edition       = {Reprint of the 1999 hardback ed.},
  isbn          = {978-0-521-11884-2},
  year          = {2009},
  publisher     = {Cambridge: Cambridge University Press},
  language      = {English},
  keywords      = {06C10,06-02,06A07},
  zbmath        = {5610899},
  zbl           = {1175.06002}
}

@Article{         Stone1935,
  author        = {Stone, M. H.},
  year          = {1935},
  title         = {Postulates for Boolean Algebras and Generalized Boolean
                  Algebras},
  journal       = {American Journal of Mathematics},
  volume        = {57},
  issue         = {4},
  doi           = {10.2307/2371008}
}

@Article{         Stone1979,
  author        = {Stone, A. H.},
  journal       = {General Topology Appl.},
  title         = {Inverse limits of compact spaces},
  year          = {1979},
  issn          = {0016-660X},
  number        = {2},
  pages         = {203--211},
  volume        = {10},
  doi           = {10.1016/0016-660x(79)90008-4},
  fjournal      = {General Topology and its Applications},
  mrclass       = {54B25},
  mrnumber      = {527845},
  mrreviewer    = {J. Segal}
}

@Book{            tao-vu,
  author        = {Tao, Terence and Vu, Van H.},
  title         = {Additive combinatorics},
  fseries       = {Cambridge Studies in Advanced Mathematics},
  series        = {Camb. Stud. Adv. Math.},
  volume        = {105},
  isbn          = {0-521-85386-9},
  year          = {2006},
  publisher     = {Cambridge: Cambridge University Press},
  language      = {English},
  keywords      = {11-02,05-02,05D10,05D40,11B75,11B13,11N13,11P70,11K31,11P82,28D05,37A45},
  zbmath        = {5066399},
  zbl           = {1127.11002}
}

@Book{            tao2010,
  author        = {Tao, Terence},
  title         = {An Epsilon of Room, I: Real Analysis: Pages from Year
                  Three of a Mathematical Blog},
  year          = 2010,
  publisher     = {American Mathematical Society},
  url           = {https://terrytao.files.wordpress.com/2010/02/epsilon.pdf}
}

@Book{            Tent_Ziegler,
  place         = {Cambridge},
  series        = {Lecture Notes in Logic},
  title         = {A Course in Model Theory},
  doi           = {10.1017/CBO9781139015417},
  publisher     = {Cambridge University Press},
  author        = {Tent, Katrin and Ziegler, Martin},
  year          = {2012},
  collection    = {Lecture Notes in Logic}
}

@Article{         tochiori_bertrand,
  author        = {Tochiori, Shigenori},
  title         = {Considering the Proof of "There is a Prime between n and
                  2n"},
  subtitle      = {Proof by a stronger estimation than the Bertrand-Chebyshev
                  theorem},
  language      = {Japanese},
  url           = {https://www.chart.co.jp/subject/sugaku/suken_tsushin/76/76-8.pdf}
}

@Book{            upmeier1987,
  author        = {Harald {Upmeier}},
  title         = {{Jordan algebras in analysis, operator theory, and quantum
                  mechanics}},
  fjournal      = {{Regional Conference Series in Mathematics}},
  journal       = {{Reg. Conf. Ser. Math.}},
  issn          = {0160-7642},
  volume        = {67},
  isbn          = {0-8218-0717-X},
  pages         = {viii + 85},
  year          = {1987},
  publisher     = {Providence, RI: American Mathematical Society (AMS)},
  language      = {English},
  msc2010       = {17-02 46-02 17C65 46H70 32M15 46G20 46L70 47B35 81Q99},
  zbl           = {0608.17013}
}

@Article{         Vaisala_2003,
  author        = {Jussi Väisälä},
  title         = {A Proof of the Mazur-Ulam Theorem},
  year          = 2003,
  journal       = {The American Mathematical Monthly},
  volume        = 110,
  number        = 7,
  publisher     = {Taylor & Francis, Ltd. on behalf of the Mathematical
                  Association of America},
  pages         = {633-635},
  url           = {https://www.jstor.org/stable/3647749},
  doi           = {10.2307/3647749}
}

@Article{         van_der_hoeven,
  author        = {van der Hoeven, Joris},
  year          = {2001},
  month         = {12},
  pages         = {},
  title         = {Operators on generalized power series},
  volume        = {45},
  journal       = {Illinois Journal of Mathematics},
  doi           = {10.1215/ijm/1258138061}
}

@Book{            wall2018analytic,
  title         = {Analytic Theory of Continued Fractions},
  author        = {Wall, H.S.},
  isbn          = {9780486830445},
  series        = {Dover Books on Mathematics},
  year          = {2018},
  publisher     = {Dover Publications}
}

@Book{            wasserman2003,
  author        = {Wasserman, Larry},
  title         = {All Of Statistics: A Concise Course in Statistical
                  Inference},
  year          = 2004,
  publisher     = {Springer}
}

@Misc{            wedhorn_adic,
  author        = {Torsten Wedhorn},
  title         = {Adic Spaces},
  year          = {2019},
  eprint        = {arXiv:1910.05934}
}

@Book{            weidmann_linear,
  author        = {Weidmann, Joachim},
  title         = {Linear operators in {H}ilbert spaces},
  isbn          = {0-387-90427-1},
  series        = {Graduate Texts in Mathematics},
  volume        = {68},
  note          = {Translated from the German by Joseph Sz\"{u}cs},
  publisher     = {Springer},
  year          = {1980},
  pages         = {xiii+402}
}

@Misc{            welzl_garter,
  author        = {Emo Welzl and Bernd G\"{a}rtner},
  title         = {Cone Programming},
  url           = {https://ti.inf.ethz.ch/ew/lehre/ApproxSDP09/notes/conelp.pdf}
}

@TechReport{      zaanen1966,
  author        = {Zaanen, A. C.},
  title         = {Lectures on "Riesz Spaces"},
  institution   = {Euratom},
  year          = {1966},
  number        = {EUR 3140.e}
}

@Article{         zbMATH06785026,
  author        = {John F. {Clauser} and Michael A. {Horne} and Abner
                  {Shimony} and Richard A. {Holt}},
  title         = {{Proposed experiment to test local hidden-variable
                  theories}},
  fjournal      = {{Physical Review Letters}},
  journal       = {{Phys. Rev. Lett.}},
  issn          = {0031-9007; 1079-7114/e},
  volume        = {23},
  pages         = {880--883},
  year          = {1969},
  publisher     = {American Physical Society (APS), New York, NY},
  language      = {English},
  msc2010       = {81-05},
  zbl           = {1371.81014},
  doi           = {10.1103/PhysRevLett.23.880},
  url           = {https://doi.org/10.1103/PhysRevLett.23.880}
}

@Article{         zorn1937,
  author        = {Zorn, Max},
  title         = {On a theorem of {E}ngel},
  journal       = {Bull. Amer. Math. Soc.},
  fjournal      = {Bulletin of the American Mathematical Society},
  volume        = {43},
  year          = {1937},
  number        = {6},
  pages         = {401--404},
  issn          = {0002-9904},
  mrclass       = {DML},
  mrnumber      = {1563550},
  doi           = {10.1090/S0002-9904-1937-06565-7},
  url           = {https://doi.org/10.1090/S0002-9904-1937-06565-7}
}
